T:Type, P:(i:Id{k:Knd| hasloc(k;i)} T), ik:LocKnd. let i,k:LocKnd = ik in P(i,k)  T 

latex

Definitions	LocKnd, let i,k:LocKnd = ik in P(i;k), x(s1,s2), f(a), Type, {x:A| B(x)} , t.1, t.2, x. t(x), x.A(x), Atom$n, Id, left + right, s ~ t, , s = t, Knd, SQType(T), {T}, P  Q, P & Q, <a, b>, x:A  B(x), P  Q, let x,y = A in B(x;y), P  Q, x:AB(x), b, hasloc(k;i), x:A. B(x), t  T
Lemmas	hasloc wf, assert wf, Knd sq, Knd wf, Id sq, Id wf, pi2 wf, pi1 wf